package puf.m2.automaton.converter;

import java.util.ArrayList;

import puf.m2.automaton.AbstractFiniteAutomaton;
import puf.m2.automaton.Automaton;
import puf.m2.automaton.State;
import puf.m2.automaton.Transition;


/**
 * The Automaton checker can be used to determine certain properties about
 * automata.
 */

public class AutomatonChecker {
    /**
     * Creates instance of <CODE>AutomatonChecker</CODE>.
     */
    private AutomatonChecker() {
    }

    public static AutomatonChecker getChecker() {
        return new AutomatonChecker();
    }

    /**
     * Returns true if <CODE>automaton</CODE> is a non-deterministic finite
     * state automaton.
     *
     * @param automaton
     *            the automaton.
     * @return true if <CODE>automaton</CODE> is a non-deterministic finite
     *         state automaton.
     */
    public boolean isNFA(Automaton automaton) {
        if (!(automaton instanceof AbstractFiniteAutomaton)) {
            return false;
        }
        State[] nondeterministicStates = getNondeterministicStates(automaton);
        return nondeterministicStates.length > 0;
    }

    /**
     * Returns an array of states that have nondeterminism.
     *
     * @return an array of states that have nondeterminism.
     */
    private State[] getNondeterministicStates(Automaton automaton) {
        EpsilonTransitionChecker checker = EpsilonTransitionChecker.getChecker();
        ArrayList<State> list = new ArrayList<State>();
        /* Get all states in automaton. */
        State[] states = automaton.getStates();
        /* Check each state for nondeterminism. */
        for (int k = 0; k < states.length; k++) {
            State state = states[k];
            /* Get all transitions from each state. */
            Transition[] transitions = automaton.getTransitionsFromState(state);

            for (int i = 0; i < transitions.length; i++) {
                Transition t1 = transitions[i];
                /* if is lambda transition. */
                if (checker.isEpsilonTransition(t1)) {
                    if (!list.contains(state))
                        list.add(state);
                }
                /*
                 * Check all transitions against all other transitions to see if
                 * any are equal.
                 */
                else {
                    for (int p = (i + 1); p < transitions.length; p++) {
                        Transition t2 = transitions[p];
                        if (areNondeterministic(t1, t2)) {
                            if (!list.contains(state))
                                list.add(state);
                        }
                    }
                }
            }
        }
        return (State[]) list.toArray(new State[0]);
    }

    /**
     * Returns true if the transitions are identical (i.e. the labels are
     * equivalent), or if they introduce nondeterminism (e.g. the label of one
     * could be a prefix of the label of the other).
     *
     * @param t1
     *            a transition
     * @param t2
     *            a transition
     * @return true if the transitions are nondeterministic.
     */
    private boolean areNondeterministic(Transition t1, Transition t2) {
        if (t1.label().equals(t2.label()))
            return true;
        else if (t1.label().startsWith(t2.label()))
            return true;
        else if (t2.label().startsWith(t1.label()))
            return true;
        else
            return false;
    }
}
